COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\bsect{Combination Modes}
C00005 ENDMK
C⊗;
\bsect{Combination Modes}
Let \compatible\ be a compatibility function for a set \mode.
The extension $\compatible\hbox{\hskip1pt}\sup\prime$ of \compatible\
to \comb\ is
$$\compprime(\Xscr,\Yscr) ={ \left \{
{\ctwocol
{\false	\lft{if there exists an $\Xscr\sup\prime$ in
\X\ and $\Yscr\sup\prime$ in
\Y\ such that}\cr
	\lft{\fcomp{\Xscr\sup\prime}{\Yscr\sup\prime}}\cr
\true	\lft{otherwise}\cr
}}\right. }$$
where \X\ and \Y\ are members of \comb.
\yskip
\defn
Let \compatible\ be the compatibility function for a set \mode\
of lock modes.
The extension $\compprime$ of \compatible\ to \update\ is:
$$\compprime(\Xscr,\Yscr)= { \left \{
\ctwocol
{\lft{$\compatible(\Xscr,\Yscr)$}	\lft{if \X\ and \Y\ are in \mode}\cr
\lft{$\compatible(\Xscr,\Yscr\sub 2)$}	\lft{if \X\ is in \mode\ and \Y\
is \up{\Yscr\sub 1}{\Yscr\sub 2}}\cr
\lft{$\compatible(\Xscr\sub 1,\Yscr)$}	\lft{if \X\ is \up{\Xscr\sub 1}{\Xscr
\sub 2}and \Y\ is in \mode}\cr
\lft{$\compatible(\Xscr\sub 1,\Yscr\sub 2)$}	\lft{if \X\ is
\up{\Xscr\sub 1}{\Xscr\sub 2} and \Y\ is \up{\Yscr\sub 1}{\Yscr\sub 2}}\cr
}\right. }$$
for \X\ and \Y\ in \update.
\yskip
Thus \ddt \up{\mup{\Xscr\sub 1}{\Xscr\sub 2}}{\Yscr} \ddt is equivalent to 
\up{\Xscr\sub 1}{\Yscr}.\ddt
Since both \up{\mup{\Xscr\sub 1}{\Xscr\sub 2}}{\Yscr} and \up{\Xscr\sub 1}{\Yscr}
have the privileges of $\Xscr\sub 1$, plus the privilege to
request a conversion to mode \Y, they are identical.
\qed
\lemma
Let \X\ be a member of \update\ and $\Yscr\sub 1$ and $\Yscr\sub 2$ be
members of \mode.
Then \up{\Xscr}{\mup{\Yscr\sub 1}{\Yscr\sub 2}} is identical to
\up{\Xscr}{\Yscr\sub 2}.
\yskip
\par